(set-logic QF_BV)
(declare-fun x () (_ BitVec 15))
(declare-fun y () (_ BitVec 11))
(declare-fun z () (_ BitVec 1))
(declare-fun b () Bool)
(assert 
(let ((e7 ((_ repeat 1) x))) 
(let ((e10 (ite (bvslt y (_ bv0 11)) (_ bv1 1) (_ bv0 1)))) 
(let ((e19 (ite (= e7 (_ bv0 15)) (_ bv1 1) (_ bv0 1)))) 
(let ((e20 (ite b (_ bv0 1) z))) 
(let ((e23 (ite (bvslt e10 z) (_ bv1 1) (_ bv0 1)))) 
(let ((e35 (ite (= ((_ zero_extend 13) z) (_ bv0 14)) (_ bv1 1) (_ bv0 1)))) 
(let ((e36 (bvsge (_ bv0 15) ((_ zero_extend 14) e19)))) 
(let ((e43 (bvslt e20 (_ bv0 1)))) 
(let ((e55 (bvslt y (_ bv0 11)))) 
(let ((e68 (distinct (_ bv0 15) ((_ sign_extend 14) e23)))) 
(let ((e79 (bvuge (_ bv0 15) x))) 
(let ((e97 (bvult (_ bv0 1) e35))) 
(let ((e110 (= ((_ zero_extend 14) e19) x))) 
(let ((e134 (xor e110 true))) 
(let ((e135 e68)) 
(let ((e137 (xor e55 e135))) 
(let ((e139 (not e36))) 
(let ((e144 (ite e97 e139 e79))) 
(let ((e148 (not e43))) 
(let ((e157 (not e137))) 
(let ((e158 (xor true e148))) 
(let ((e173 (= e144 e158))) 
(let ((e174 (= true e173))) 
(let ((e177 (=> e134 e174))) 
(let ((e180 e157)) 
(let ((e184 (=> e180 e177))) 
(let ((e187 (not e184))) 
(let ((e188 (not e187))) 
(let ((e189 (not e188))) 
(let ((e190 e189)) 
(let ((e192 e190)) 
(let ((e193 (or e192 e192))) 
(let ((e194 (and e193 e193))) 
(let ((e196 (not e194))) 
(let ((e197 (and e196 e196))) 
(let ((e200 e197)) 
(let ((e201 e200)) 
(let ((e202 e201)) e202)))))))))))))))))))))))))))))))))))))))
(check-sat)

